\begin{tabbing}
$\forall$\=${\it es}$:ES, $C$, $T$:Type, $S_{1}$, $S_{2}$:($C$$\rightarrow$$C$$\rightarrow$E$\rightarrow\mathbb{P}$),\+
\\[0ex]${\it codes}_{1}$:($j$,$i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $S_{1}$($j$,$i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$),
\\[0ex]${\it codes}_{2}$:($j$,$i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $S_{2}$($j$,$i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$),
\\[0ex]${\it dec\_S}_{1}$:($j$,$i$:$C$$\rightarrow$$e$:E$\rightarrow$Dec($S_{1}$($j$,$i$,$e$))).
\-\\[0ex][$S_{1}$? ${\it codes}_{1}$ : ${\it codes}_{2}$] $\in$ $j$,$i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ ($S_{1}$($j$,$i$,$x$)) $\vee$ ($S_{2}$($j$,$i$,$x$))\} $\rightarrow$state@loc($e$)$\rightarrow$$T$
\end{tabbing}